; <lemma>
;  <title>BoschSwitch.2</title>
;  <origin>BoschSwitch | m1 | INITIALISATION/inv1/INV</origin>
(benchmark boschswitch_2
;  <theories>
;    <theory name="linear_order_int"/>
;  </theories>
  :logic QF_LIA
  :extramacros (
		 (Nat
		  (lambda (?i Int) . (<= 0 ?i)))
		 (in (lambda (?x1 't1) (?p ('t1 boolean)) . (?p ?x1)))
		 )
; <goal>0 : NATURAL</goal>
  :formula
  (not
      (in 0 Nat)
    )
)
;</lemma>
